An introduction to formalized mathematics: why it is interesting?

Abstract: Formalization is the process of digitalizing mathematical results, teaching them to a computer. We will explain how this process is done, explaining the general philosophy behind it, and why it is interesting for people interested in ``standard'' mathematics. Indeed, formalization has several benefits, the most obvious being the verification of the correctness of theorems beyond a reasonable doubt, starting from the axioms. I will explain in detail what this means, and also why I think there are others, even more important, advantages of formalized mathematics. This is not a course in logic nor foundations of mathematics, in particular no prior knowledge of these topics is needed.

Mathematics

Audience: undergraduates

An introduction to proof assistants: a mini course about mathematical formalization

Series comments: The goal of this mini-course is to give an introduction to formalization of mathematics. I will explain what formalizing mathematics means and why it is interesting and useful for people interested in "standard" mathematics. I will show how this is done in practice using Lean, one of the several proof assistants available today. This is not a course in logic nor foundations of mathematics, in particular no prior knowledge of these topics is needed.